COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Heavy duty set theory
C00011 ENDMK
C⊗;
Heavy duty set theory

	We have used first order axiomatizations of set theory in most
of the proofs done in FOL so far including the proofs of Lagrange's theorem
in group theory, Wilson's theorem in number theory, Ramsey's theorem in
combinatorics, and in the retrospective analysis chess problem.  In each
case, we have used a standard Zermelo-Frankel axiomatization.  It has
turned out that one of the main reasons for the excessive length of the
formal proofs has been the primitive character of the set theory.  This
made necessary roundabout ways of handling functions and partial
functions and made necessary the proof of many intermediate results
that should be taken as part of set theory.

	The well-known set theories have this primitive character, because
they have been designed as the objects of metamathematical reasoning
rather than as the domains of substantive reasoning.  Our experience now
allows us to design a %2heavy duty set theory%1 within which we hope
proofs will be much shorter.  This is an important step towards making
computer checked proofs into a practical technique.


Mathematical Theory of Computation

	Unlike proof-checking and formalization of common sense facts in which
the Stanford AI Lab is essentially alone in the world, mathematical
theory of computation has become a major part of computer science and
is pursued all over the world.  It is to our advantage to point out, however,
that the term %2mathematical theory of computation%1 and some of the
major lines of investigation (representation of algorithms by recursive
definitions using conditional expressions and formal interpreter semantics)
originated in papers by McCarthy (1962,1963, 1964 and 1965), and other
pioneering work has been done in this Laboratory (Luckham, Milner, London,
Igarashi, Ashcroft, Manna, Vuillemin, Cadiou).

	At present, our work in MTC specializes in the following areas
which we think are essential for applications and are not being pursued
elsewhere:

	1. Getting the Scott theory into a form in which it can be used
in first order logic and set theory.  This seems essential if this
powerful and elegant theory is to be combined with other mathematics.
During his recent sabbatical at Kyoto University, McCarthy continued
his work on an approach to this problem using his new concept of
%2extensional forms%1.

	2. Developing formalism for expressing properties of systems
involving the physical world by parallel indeterminate programs and
using this to state the specifications of computer programs that interact
with the physical world.  Some of the programs most important to the
Defense Department are command and control programs whose correctness
involves their interaction with the physical world.

	3. Formally describing sources of information.  The idea is to
be able to describe the properties of files, interactive programs, and
human sources of information in such a way that programs that use these
sources can be proved correct.  Descriptions of data structures have been
used for many years in programming languages that set up data structures, e.g.
COBOL, but we are interested in being able to describe data structures
that other people have set up and over whose structure and representation
we have no control.  Many data structures are accessible via interactive
programs that think they are dealing with a human, and we would like to
be able to describe the interactions formally so that programs could be
designed that would obtain information from them.

	We are presently discussing with Program understanding group here
and with a group at Lawrence Berkeley Laboratory that is the proprietor
of Census and other large data files systems that can obtain answers to
questions on the basis of programs that can be given descriptions of
files and interactive programs available on the ARPA net.

	The following toy problem is being investigated: Most of the
Laboratories supported by IPT maintain lists of addresses and
telephone numbers in their computer systems, but each laboratory
has its own structure for these files.  However, these structures differ
only in minor and rather arbitrary ways like punctuation, order of items,
and the presence or absence of various kinds of additional information.
We think we can devise a way of describing such files so that a program
equipped with a description of the files can find anyone's address.

	Besides its long term scientific value, this work has potential
short term application to DoD problems.  DoD has many thousands of data
files in hundreds of computers all over the world.  Increasingly, these
computers are accessible by networks and by ordinary telephone lines.
However, there is no short term prospect of reorganizing them in any
consistent way, because each file has been optimized for its main local
application.  Some of these files have special interactive programs to
go with them, and, in fact, some of the interactive systems are specialized
to the level of the terminal, i.e. if you want to use them, you are
urged to obtain a particular terminal and put it in your office next to
your other terminals for using other systems.  If we can develop a means
of formally describing these information systems, a computer can use
such descriptions to answer a question by interacting with a file or
information system in the way in which its designers intend without the
user having to learn each information system separately.